
  \begin{context}[h]
    \begin{center}
    \begin{tabular}{|l|l|}
    \hline\hline
    {\bf Type Name} & {\bf Type}\\
    \hline\hline
    $\typ{TyBool}$ & $\typ{\Pi X. \AT{X}{\AT{X}{X}}}$ \\
    \hline\hline
    {\bf Term Name} & {\bf Term}\\
    \hline\hline
    $true$ & $\Lambda X.\la{x}{X}.\la{y}{Y}.x$\\
    $false$ & $\Lambda X.\la{x}{X}.\la{y}{Y}.y$\\ \hline\hline
    \end{tabular}
    \caption{An example context for an ABGP system that evolves boolean type functions}
    \label{BooleanTerminals}
    \end{center}
    \end{context}
\noindent
\GT{} is the type of the  program that the system is set-up to evolve.
For example, \GT{} is:
\begin{equation*}
\typ{\AT{TyBool}{\AT{TyBool}{TyBool}}}
\end{equation*}
 in a system that evolves binary boolean operators (such as $xor$) within context \ref{BooleanTerminals}.  A system that evolves programs that take a list of integers (type $\typ{(\Pi X. \AT{X}{\AT{(\AT{Int}{\AT{X}{X}})}{X})}}$) as argument and return its length, will have its \GT{} set up to be:
\begin{equation*}
\typ{\AT{(\Pi X. \AT{X}{\AT{(\AT{Int}{\AT{X}{X}})}{X})}}{Int}}
\end{equation*}
\noindent
\GT{} is a partial specification of the programs produced by the system. It specifies:
\begin{enumerate}
\item The arguments of the programs constructed by the system
\item The type of the object returned by the programs constructed by system
\end{enumerate}
\noindent
As a rule, in this work, the first argument of \GT{} will always be a data type. That is, there are types $\typ{A}$ and $\typ{B}$ such that both \ref{predeco1} and \ref{predeco2} always hold:
\begin{align}
\label{predeco1}
(ty\_eqv\ \GT\ \typ{\AT{A}{B}}) & = true \\
\label{predeco2}
(\mathit{is\_data\_type}\ A) & = true
\end{align}